\begin{tabbing}
$\forall$$T$,$A$:Type, $f$:($A$$\rightarrow$$T$), $l$:IdLnk.
\\[0ex]normal{-}type\=\{i:l\}\+
\\[0ex]($A$)
\-\\[0ex]$\Rightarrow$ normal{-}type\=\{i:l\}\+
\\[0ex]($T$)
\-\\[0ex]$\Rightarrow$ es{-}real\=\{i:l\}\+
\\[0ex](\=${\it es}$.locl(mkid\{b:ut2\}) sends [mkid\{tg:ut2\},$f$\{$A$$\rightarrow$$T$\}(mkid\{done:ut2\})] on link $l$ once\+
\\[0ex])
\-\-
\end{tabbing}